UseWitness if $a$=$b$ then inl Ax  else (inr ($\lambda$$x$.$x$) )